g:OMon. Linorder(|g|;x,y.(x  y)) 

latex

Up	groups 1
Definitions of Statement	Mon, AbMon, OMon
Definitions	t  T, True, T, x:A. B(x), x,y. t(x;y), , Order(T;x,y.R(x;y)), P & Q, x f y, Linorder(T;x,y.R(x;y)), P  Q, SqStable(P), OMon, Mon, x(s1,s2), AbMon
Lemmas	omon wf, sq stable connex, sq stable anti sym, sq stable trans, decidable assert, sq stable from decidable, sq stable refl, connex wf, anti sym wf, trans wf, grp le wf, assert wf, grp car wf, refl wf, sq stable and